\section{Subject}\label{sec:impl-subject}
Subjects are the main components that are executed on top of the kernel, as
described in section \ref{sec:design-subject}. They are represented using two
main data structures: subject specification and subject state.

\subsection{Specification}
A subject is specified in the global system policy. The XML specification
precisely defines the execution environment and granted resources. The
information that is relevant to the kernel is part of the compiled policy.
Listing \ref{lst:skp-subjects} presents the SPARK type specification into which
all subject related policy parts are transformed. The specification of a subject
is static and cannot be changed at runtime since it is declared as a constant
data structure.

\lstinputlisting[
	language=ada,
	linerange={32-51},
	label=lst:skp-subjects,
	caption=SPARK subject spec type]
	{files/skp-subjects.adb}

\subsection{State}
The system state related to a subject must encompass all resources that it can
control directly or indirectly. This is necessary to enable the scheduler to
preempt a subject by preserving its state and seamlessly resume execution at a
later stage by restoring the previously saved state.

Additionally, separation of subjects demands that unintended information flow
due to subject switching must be prevented. This is only achievable if the
subject state that is saved and restored encompasses every element of the
systems environment that is accessible by more than one subject. While the Intel
VMX extensions save and restore parts of the subject state automatically to and
from the associated VMCS on VMX transition, others must be handled manually by
the kernel. Listings \ref{lst:sk-subject-state} and \ref{lst:sk-cpu-registers}
show the record types used by the Kernel to maintain the state of a subject.

\lstinputlisting[
	language=ada,
	linerange={58-74},
	label=lst:sk-subject-state,
	caption=SPARK subject state type]
	{files/sk.ads}

\lstinputlisting[
	language=ada,
	linerange={37-53},
	label=lst:sk-cpu-registers,
	caption=SPARK CPU registers type]
	{files/sk.ads}

A SM\index{SM} subject may access the state of a given subject. This enables
the SM to alter a subject's state and thus perform emulation. Because a subject
is not allowed to access the VMCS structure of another subject, the kernel also
copies register values managed automatically by VMX\index{VMX} into the
in-memory subject state to enable modification by the SM subject.

During subject setup, the state is initialized to zero. This is done by
assigning the \texttt{Null} subject state constants shown by listings
\ref{lst:sk-null-subject-state} and \ref{lst:sk-null-cpu-registers} to all
state variables.

\lstinputlisting[
	language=ada,
	linerange={120-136},
	label=lst:sk-null-subject-state,
	caption=SPARK null subject state constant]
	{files/sk.ads}

\lstinputlisting[
	language=ada,
	linerange={103-118},
	label=lst:sk-null-cpu-registers,
	caption=SPARK null CPU registers constant]
	{files/sk.ads}

The initialization of the subject state is then completed by copying the code
entry point and the address of the stack from the specification.  These values
are declared in the system policy as part of the subject initial state and can
be obtained automatically from a native subject binary by using the
\texttt{skconfig} tool (see section \ref{subsec:subject-binary-analysis}).
